i:Id, ds:x:Id fp Type, da:k:Knd fp Type, A:ecl(ds;da), snd:msg-spec(ds;da),
upd:update-spec(ds;da), es:ES.
msg-spec-loc(snd;i)  update-spec-decl(upd;ds)  @i[[A;snd;upd]]  Prop 

latex

Definitions

t  T, P  Q, x:A. B(x), update-spec-decl(upd;ds), Atom$n, Id, x:A. B(x), (x  l), b, Type, x.A(x), x. t(x), a:A fp B(a), Top, x:AB(x), IdDeq, x  dom(f), True, T, SqStable(P), {x:A| B(x) }, msg-spec-loc(snd;i), x:AB(x), IdLnk, source(l), <a,b>, s = t, Knd, ecl(ds;da), msg-spec(ds;da), update-spec(ds;da), ES, update-spec-vars(upd), @i[[x;upd]], xL.P(x), msg-spec-links(snd), @i[[x;snd]], Prop, P & Q, @i[[x;snd;upd]]

Lemmas

ecl-mng-sends wf, IdLnk wf, msg-spec-links wf, l-all wf, ecl-mng-update wf, l member wf, update-spec-vars wf, update-spec-decl wf, msg-spec-loc wf, event system wf, update-spec wf, msg-spec wf, ecl wf, Knd wf, fpf wf, sq stable from decidable, decidable assert, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, Id wf